Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Update dead link to grepcode #436

Merged
merged 1 commit into from
Dec 7, 2018
Merged

Update dead link to grepcode #436

merged 1 commit into from
Dec 7, 2018

Conversation

aki-ks
Copy link
Contributor

@aki-ks aki-ks commented Oct 14, 2018

Grepcode is dead. openjdk.java.net should be more lasting.

@aki-ks
Copy link
Contributor Author

aki-ks commented Oct 15, 2018

That's strange. I've just changed a comment. How can this cause the build to fail?

@Hydrotoast
Copy link
Contributor

Hi @aki-ks , I checked the build failure. I ran into the same issue in #438, which is a flaky test that occurs with a frequency of 1 / 1000 per build job (I believe there are ~10-15 build jobs per PR). The PR includes a fix in the second commit.

Due to the rarity of the flakiness, you can trigger a new build that should pass with a high probability of success. A build should be triggered when this PR detects a change in the source branch of the merge, which appears to be patch-1 of your repository.

I believe you can amend the the timestamp of the commit without changing the diff or the message and force push to your patch-1 branch. The following should work, but be sure that you are on the branch that has the desired change. :)

git commit --amend --no-edit
git push -f origin patch-1

@rickynils rickynils merged commit a10ce6d into typelevel:master Dec 7, 2018
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants